COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	propositional schemata, used by the rewriter to normalize expressions
C00004 ENDMK
C⊗;
;propositional schemata, used by the rewriter to normalize expressions
(wipe-out)
(proof normal)

;1
(axiom  |∀p q r.((p∨q)∧r)≡((p∧r)∨(q∧r))|)
(label normal)

;2
(axiom  |∀p q r.(r∧(p∨q))≡((r∧p)∨(r∧q))|)
(label normal)

;3
(axiom  |∀p q r.(r∧(p∨q))≡((p∧r)∨(q∧r))|)
(label normal)
;4
(axiom |∀p q r.(p∨q⊃r)≡(p⊃r)∧(q⊃r)|)
(label normal)

;5
(axiom  |∀p q.(¬(p∨q))≡((¬p)∧(¬q))|)
(label demorgan)

;6
(axiom |∀p q.¬(p∧q)≡¬p∨¬q|)
(label demorgan1)

;It would cause combinatorial explosion,to add these to simpinfo, or to put everything,
;say,in conjunctive normal form. So we call them as rewriters when needed.

;a few tricks

;7
(axiom |∀p q.p≡(q⊃p)∧(¬q⊃p)|)
(label excluded_middle)

;8
(derive |∀p q r.(q⊃r)∧(if p then q else r)⊃r|)
(label trans_cond)

(save-proofs normal)